package at.tasat.test.level3;

import java.io.ByteArrayInputStream;
import java.io.IOException;
import java.util.Arrays;
import java.util.Comparator;
import java.util.Random;
import java.util.SortedSet;
import java.util.TreeSet;

import at.tasat.assignment.Assignment;
import at.tasat.cnf.Cnf;
import at.tasat.parser.DimacsParser;
import at.tasat.solver.Solver;
import at.tasat.solver.SolverException;

public class DimacsFuzzer {

	public static void main(String[] args) throws IOException, InterruptedException, SolverException {
		String dimacsString = getRandomCnf(120, 7000); 
		Cnf cnf = DimacsParser.parse(new ByteArrayInputStream(dimacsString.getBytes()));
		Solver solver = Solver.create(cnf);
		boolean sat = solver.solve();
		if (sat) {
			System.out.println("SAT:");
			Assignment[] assignments = solver.getAssignment().getAllAssignments();
			Arrays.sort(assignments, new AssignmentComparator());
			for (Assignment assignment : assignments) {
				System.out.println("x_" + assignment.getVariableId() + " = " + assignment.getPhase());
			}
		} else {
			System.out.println("UNSAT");
		}
		solver.releaseThreadManager();
	}
	private final static class AssignmentComparator implements Comparator<Assignment> {

		@Override
		public int compare(Assignment a1, Assignment a2) {
			return Integer.compare(a1.getVariableId(), a2.getVariableId());
		}
		
	}

	public static String getRandomCnf(int variables, int clauses) {
		return getRandomCnf(variables, clauses, (int) System.currentTimeMillis());
	}

	public static String getRandomCnf(int variables, int clauses, long seed) {
		assert variables > 0;
		assert clauses > 0;
		long variableOccurencesSum = (long) variables * (long) clauses;
		int[] variableOccurences = new int[variables];
		for (int i = 0; i < variables; i++) {
			variableOccurences[i] = clauses;
		}
		Random random = new Random(seed);

		StringBuilder builder = new StringBuilder();
		appendHeader(builder, variables, clauses, seed);

		for (int clause = 0; clause < clauses; clause++) {
			SortedSet<Integer> usedVariables = new TreeSet<Integer>();
			int numVariables = random.nextInt(variables / 2 + 1) + 1;
			for (int variable = 0; variable <= numVariables; variable++) {
				long value = (long) (variableOccurencesSum * random.nextDouble());
				int variableId = getVariableId(value, variableOccurences);
				if (usedVariables.add(variableId)) {
					variableOccurences[variableId - 1]--;
					variableOccurencesSum--;
				}
			}
			if (clause == clauses - 1) {
				appendNeverUsedVariables(usedVariables, variableOccurences, variables, clauses);
			}
			appendClause(builder, usedVariables, random);
		}

		return builder.toString();
	}

	private static void appendHeader(StringBuilder builder, int variables, int clauses, long seed) {
		builder.append("c seed=");
		builder.append(seed);
		builder.append("\n");
		builder.append("p cnf ");
		builder.append(variables);
		builder.append(' ');
		builder.append(clauses);
	}

	private static void appendNeverUsedVariables(SortedSet<Integer> usedVariables, int[] variableOccurences, int variables, int initialValue) {
		for (int i = 0; i < variables; i++) {
			if (variableOccurences[i] == initialValue) {
				usedVariables.add(i + 1);
			}
		}
	}

	private static void appendClause(StringBuilder builder, SortedSet<Integer> usedVariables, Random random) {
		builder.append("\n");
		for (Integer variable : usedVariables) {
			int literal = random.nextBoolean() ? variable : -variable;
			builder.append(literal);
			builder.append(' ');
		}
		builder.append("0");
	}

	private static int getVariableId(long value, int[] variableOccurences) {
		for (int i = 0; i < variableOccurences.length; i++) {
			value -= variableOccurences[i];
			if (value <= 0) {
				return i + 1;
			}
		}
		throw new RuntimeException("not possible");
	}
}
